MAYBE 47.552 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could not be shown:



↳ HASKELL
  ↳ LR

mainModule Monad
  ((mapAndUnzipM :: (b  ->  Maybe (c,a))  ->  [b]  ->  Maybe ([c],[a])) :: (b  ->  Maybe (c,a))  ->  [b]  ->  Maybe ([c],[a]))

module Monad where
  import qualified Maybe
import qualified Prelude
  mapAndUnzipM :: Monad a => (d  ->  a (c,b))  ->  [d]  ->  a ([c],[b])
mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip


module Maybe where
  import qualified Monad
import qualified Prelude


Lambda Reductions:
The following Lambda expression
\(a,b)~(as,bs)→(a : as,b : bs)

is transformed to
unzip0 (a,b) ~(as,bs) = (a : as,b : bs)

The following Lambda expression
\xs→return (x : xs)

is transformed to
sequence0 x xs = return (x : xs)

The following Lambda expression
\x→sequence cs >>= sequence0 x

is transformed to
sequence1 cs x = sequence cs >>= sequence0 x



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IPR

mainModule Monad
  ((mapAndUnzipM :: (b  ->  Maybe (a,c))  ->  [b]  ->  Maybe ([a],[c])) :: (b  ->  Maybe (a,c))  ->  [b]  ->  Maybe ([a],[c]))

module Maybe where
  import qualified Monad
import qualified Prelude

module Monad where
  import qualified Maybe
import qualified Prelude
  mapAndUnzipM :: Monad a => (c  ->  a (b,d))  ->  [c]  ->  a ([b],[d])
mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip



IrrPat Reductions:
The variables of the following irrefutable Pattern
~(as,bs)

are replaced by calls to these functions
unzip00 (as,bs) = as

unzip01 (as,bs) = bs



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IPR
        ↳ HASKELL
          ↳ BR

mainModule Monad
  ((mapAndUnzipM :: (a  ->  Maybe (c,b))  ->  [a]  ->  Maybe ([c],[b])) :: (a  ->  Maybe (c,b))  ->  [a]  ->  Maybe ([c],[b]))

module Monad where
  import qualified Maybe
import qualified Prelude
  mapAndUnzipM :: Monad d => (a  ->  d (c,b))  ->  [a]  ->  d ([c],[b])
mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip


module Maybe where
  import qualified Monad
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IPR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR

mainModule Monad
  ((mapAndUnzipM :: (a  ->  Maybe (b,c))  ->  [a]  ->  Maybe ([b],[c])) :: (a  ->  Maybe (b,c))  ->  [a]  ->  Maybe ([b],[c]))

module Maybe where
  import qualified Monad
import qualified Prelude

module Monad where
  import qualified Maybe
import qualified Prelude
  mapAndUnzipM :: Monad b => (c  ->  b (d,a))  ->  [c]  ->  b ([d],[a])
mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IPR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL

mainModule Monad
  (mapAndUnzipM :: (c  ->  Maybe (b,a))  ->  [c]  ->  Maybe ([b],[a]))

module Monad where
  import qualified Maybe
import qualified Prelude
  mapAndUnzipM :: Monad d => (c  ->  d (a,b))  ->  [c]  ->  d ([a],[b])
mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip


module Maybe where
  import qualified Monad
import qualified Prelude